Search for: All records

Abstract Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement ofhyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We studyblack-vs.gray-vs.white-boxenforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants. 

Runtime verificationis a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronousdistributedmonitors observing the system, only if each monitor can emit verdicts taken from alarge enoughfinite set. We revisit this impossibility result in the concrete context of linear-time logic (ltl) semantics for runtime verification, that is, when the correctness of the system is specified by anltlformula on its execution traces. First, we show that monitors synthesized based on the 4-valued semantics ofltl(rv-ltl) may result in inconsistent distributed monitoring, even for some simpleltlformulas. More generally, given anyltlformula φ, we relate the number of different verdicts required by the monitors for consistently monitoring φ, with a specific structural characteristic of φ called itsalternation number. Specifically, we show that, for everyk ≥ 0, there is anltlformula φ with alternation number kthat cannot be verified at runtime by distributed monitors emitting verdicts from a set of cardinality smaller thank+ 1. On the positive side, we define a family of logics, calleddistributedltl(abbreviated asdltl), parameterized byk≥ 0, which refinesrv-ltlby incorporating2k+ 4 truth values. Our main contribution is to show that, for everyk≥ 0, everyltlformula φ with alternation number kcan be consistently monitored by distributed monitors, each running an automaton based on a (2 ⌈k/2 ⌉ +4)-valued logic taken from thedltlfamily.